$\forall$$a$:$\mathbb{N}$, $b$:$\mathbb{N}^{+}$. $\exists$$q$:$\mathbb{N}$. $\exists$$r$:int\_seg(0; $b$). ($a$ = (($q$ $\ast$ $b$) + $r$) $\in$ $\mathbb{Z}$)